a:{...0}, n:. (a rem n) = (-((-a) rem n)) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), P & Q, P  Q, P  Q, False, P  Q, A, a  b  T , A  B, , {...i}, S  T
Lemmas	int lower wf, nat plus wf, minus functionality wrt eq, rem to div, nat plus inc int nzero, div 2 to 1